Coq (proof assistant system)
Public.icon
Coq - Wikipedia
Coq is a proof assistant system. The core of Coq uses the programming language Gallina. It is being developed by the PI.R2 team of the French National Institute for Computer Science and Control (located within the PPS research institute), in collaboration with École Polytechnique, the National School of Arts and Crafts, Paris Diderot University, Paris-Sud University (formerly also with the École Normale Supérieure de Lyon). Hugo Herbelin is the de facto development leader.
About the theorem proving system Coq
What is a theorem proving system and what can it do? | Morikita Publishing | note
https://gyazo.com/ba3b9998bf258aa44a727ab3ff480349